Nuprl Lemma : w-Msg-from_wf
0,22
postcript
pdf
the_w
:World,
i
:Id. MsgFrom(
i
)
Type
latex
Definitions
World
,
MsgFrom(
i
)
,
Msg
,
w
.M
,
Msg(
M
)
,
source(
l
)
,
mlnk(
m
)
,
x
:
A
.
B
(
x
)
,
t
T
,
Id
Lemmas
Id
wf
,
mlnk
wf
,
lsrc
wf
,
Msg
wf
,
world
wf
origin
the_w:World, i:Id. MsgFrom(i) 
Type the_w:World, i:Id. MsgFrom(i) Type x:A. B(x) T